sub-es-pred(es;dom;e)
== if first(e) then inr   if dom(pred(e)) then inl pred(e)  else sub-es-pred(es;dom;pred(e)) fi 

---

clarification:

sub-es-pred(es;dom;e)
== if es-first(es; e)
== ifthen inr  
== if dom(es-pred(es; e)) then inl es-pred(es; e)  else sub-es-pred(es;dom;es-pred(es; e)) fi 
(recursive) 

latex

Definitions	Y, x.A(x), first(e), inr x , , if b then t else f fi , inl x , f(a), pred(e)
FDL editor aliases	sub-es-pred